#ifndef __DPLL_H__
#define __DPLL_H__

#include"solver.h"
typedef struct _dpllresult{
    _bool sat;
    cnf* model_cnf;
}dpllresult;

typedef struct _unit_pair{
    variable* var;
    clause* cls;
}unit_pair;

variable* find_first_unassigned(variable* vars, int nvar);

_bool ALL_CLAUSES_ARE_TRUE(clause* cls_set, int ncls);
_bool ONE_CLAUSE_IS_FALSE(clause* cls_set, int ncls);

_bool dpll_satisfiable(cnf*_cnf);



/**
 * Goes through the cnf formula and looks for a unit clause
 * @param cnf the cnf object that represents the original formula and a partial model (var->value assignment)
 * @return the variable of the unit clause if it found one, nullptr otherwise
 */
variable* FIND_UNIT_CLAUSE(cnf* cnf);
unit_pair* FIND_UNIT_CLAUSE_P(cnf* cnf, _bool seq);

/**
 * sets a given variable to a given value in the whole cnf
 */
void set_variable_value(cnf* cnf, variable* var, _bool value);
void unset_variable_value(cnf* cnf, variable* var);

void set_variable_flag_all(cnf* cnf, variable* var, short flag);

/**
 * Goes through the cnf formula and looks for a pure variable
 * @param cnf the cnf object that represents the original formula and a partial model (var->value assignment)
 * @return a pure variable if it found one, nullptr otherwise
 */
variable* FIND_PURE_VAR(cnf* cnf);

/**
 * Handles the branching of DPLL, if we need to make a decision, it either calls the callback function registered in the
 * config or runs both branches recursively
 *
 * The first option is used in the standard setting (sequential)
 * The second option is used in the parallel setting
 */
dpllresult* branch_on_variable(variable* var, cnf* cnf);

/**
 * Run dpll on a given cnf object
 * @param cnf the cnf object that represents the original formula and a partial model (var->value assignment)
 * @return DpllResult object
 */
dpllresult* DPLLalgorithm(cnf* cnf);

#endif